i:Id, X, T:Type, x0:X, P:(XTProp).
Normal(T)
 Normal(X)
 (x:X. Dec(v:T. P(x,v)))
 preinit1R{x:ut2, a:ut2}(i; X; T; x0; P)  Realizer 

latex

Definitions	if b t else f fi, s.x, preinit1R{$x:ut2, $a:ut2}(i; X; T; x0; P), P  Q, true, Top, x:A. B(x), x:A. B(x), Prop, x. t(x), t  T, Id, x(s), State(ds)
Lemmas	normal-type wf, decidable wf, subtype rel self, fpf-single wf, Rlist wf, id-deq wf, eqof eq btrue, Rpre wf, Id wf, Rinit wf, fpf-cap-single